x declared in M == x  dom(1of(M)) 

latex

---

clarification:

x declared in M == fpf-dom(IdDeq; x; 1of(M)) 

latex

Definitions	b, x  dom(f), IdDeq, 1of(t)
FDL editor aliases	ma-declx